﻿using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Microsoft.Pex.Framework;

namespace AutomaTones.Model.Automaton_Model {
    /// <summary>
    /// A cell with a given state decided by one or more rules.
    /// Multiple triggers can be attached to react to different states - by publishing events.
    /// </summary>
    /// <author>Anders Øland / anoe@itu.dk</author>
    [Serializable]
    public class Cell {
        /// <summary>
        /// The state of the cell.
        /// </summary>
        public State State { get; protected internal set; }
        
        /// <summary>
        /// The rule governing the state & evolution of this cell
        /// </summary>
        public Rule Rule { get; protected internal set; }
        
        public Cell(Rule rule, int stateMin = 0, int stateMax = 1, int stateInit = 0) {
            Contract.Requires(null != rule);
            Contract.Requires(stateMin < stateMax);
            Contract.Requires(stateMin <= stateInit && stateMax >= stateInit);
            Contract.Ensures(Rule.Equals(rule));
            Contract.Ensures(State.SpaceMin == stateMin && State.SpaceMax == stateMax && State.CurrentState == stateInit);
            Rule = rule;
            State = new State(stateMin, stateMax, stateInit);
        }

        [ContractInvariantMethod]
        private void ObjInvariant() {
            Contract.Invariant(null != State);
            Contract.Invariant(null != Rule);
        }
    }
}
